<,+>  OCMon 

latex

Up	groups 1
Definitions of Statement	GrpSig, |g|, =, , *, e, Mon, AbMon, Group{i}, AbGrp, IsMonHom{M1,M2}(f), IsMonHomInj(g;h;f), OCMon, OGrp, <+>, <,+>
Definitions	t  T, x,y. t(x;y), , t.1, <+>, x f y, P & Q, |g|, x:A. B(x), P  Q, t.2, , x:A. B(x), e, *, FunThru2op(A;B;opa;opb;f), Inj(A;B;f), IsMonHom{M1,M2}(f), <,+>, IsMonHomInj(g;h;f), P  Q, P  Q, =, RelsIso(T;T';x,y.R(x;y);x,y.R'(x;y);f), , AbMon, x(s1,s2), Mon, Group{i}, AbGrp, OCMon, OGrp, False, A, A  B, S  T
Lemmas	nat add mon wf, inj into ocmon, grp le wf, grp eq wf, assert wf, rels iso wf, abgrp wf, grp sig inc, int add grp wf, mon hom inj p wf, grp car wf, ocgrp wf, int add grp wf2, le wf, nat wf, eq int wf, le int wf